open import Relation.Unary using ( Pred ; U; Decidable )
open import Algebra.Structures using (  IsGroup ; IsAbelianGroup ; IsSemigroup)
open import Algebra using ( Group ; Monoid ; Semigroup ; AbelianGroup)
open import Relation.Binary using ( Rel )
open import Algebra.FunctionProperties using ( Op₁ ; Op₂ )
open import Level using ( Level ; _⊔_ ; suc )
open import Data.Product using ( _×_ ; _,′_ ; proj₁ ; proj₂ ; _,_) 
open import Relation.Binary.Core using (IsEquivalence ; _Respects_ ; _Respects₂_ )
open import Algebra.Structures

module Substructures where
_ClosedUnder_ : {a b : Level} {A : Set a} (pred : Pred A b) → (∙ : Op₂ A) → Set (a ⊔ b)
_ClosedUnder_ pred _∙_ =  ∀ {x y} → pred x → pred y → pred (x ∙ y)

_ClosedUnder₁_ : {a b : Level} {A : Set a} (pred : Pred A b) → (_⁻¹ : Op₁ A) → Set (a ⊔ b)
_ClosedUnder₁_ pred _⁻¹ =  ∀ {x} → pred x → pred (x ⁻¹)

record IsSubMonoid {a b ℓ} {A : Set a} (_≈_ : Rel A ℓ) (I : Pred A b) (_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ ⊔ b) where
  field
    isMonoid : IsMonoid _≈_ _∙_ ε
    ∙_isSubStructure : I ClosedUnder _∙_
    ≈_respect : I Respects _≈_
    εInSubset : I ε
    
record IsSubGroup {a b ℓ : Level} {A : Set a} (_≈_ : Rel A ℓ) (subsetPred : Pred A b) (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ ⊔ b) where
  field
    isGroup : IsGroup _≈_ _∙_ ε _⁻¹
    isSubMonoid : IsSubMonoid _≈_ subsetPred _∙_ ε
    ⁻¹_isSubStructure : subsetPred ClosedUnder₁ _⁻¹

  open IsGroup isGroup public
  open IsSubMonoid isSubMonoid public

record IsSubAbelianGroup {a b ℓ : Level} {A : Set a} (_≈_ : Rel A ℓ) (I : Pred A b) (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ ⊔ b) where
  field
    isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε _⁻¹
    isSubGroup : IsSubGroup _≈_ I _∙_ ε _⁻¹

  open IsAbelianGroup isAbelianGroup public
  open IsSubGroup isSubGroup --DOZRO


record SubGroup c b ℓ : Set (suc (c ⊔ ℓ ⊔ b)) where
  infix  8 _⁻¹
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    IsInSubset : Pred Carrier b
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    ε       : Carrier
    _⁻¹     : Op₁ Carrier
    isSubGroup : IsSubGroup _≈_ IsInSubset _∙_ ε _⁻¹

  open IsSubGroup isSubGroup public

  group : Group c ℓ 
  group = record { isGroup  = isGroup }

  open Group group public using (semigroup; monoid; rawMonoid)

-- + normal subgroup
IsNormalIn : {a b c : Level} (A : Set a) (normalInWhat : Pred A c)
             (I : Pred A b) (_∙_ : Op₂ A) (_⁻¹ : Op₁ A) → Set (a ⊔ b ⊔ c)
IsNormalIn A normalInWhat I _∙_ _⁻¹ = (a : A) → {_ : normalInWhat a} →
           (x : A) → (_ : I x) → (I ((a ∙ x) ∙ (a ⁻¹)))

IsNormalInG : {a b ℓ c : Level} {A : Set a} {_≈_ : Rel A ℓ} {I : Pred A b}
  {_∙_ : Op₂ A} {ε : A} {_⁻¹ : Op₁ A} (isSubG : IsSubGroup _≈_ I _∙_ ε _⁻¹)
  (normalInWhat : Pred A c) → Set (a ⊔ b ⊔ c)
IsNormalInG {a} {b} {ℓ} {c} {A} {_≈_} {subsetPred} {_∙_} {ε} {_⁻¹} isSubG normalInWhat =
  IsNormalIn A normalInWhat subsetPred _∙_ _⁻¹  

record IsNormalSubGroup {a b ℓ : Level} {A : Set a} (_≈_ : Rel A ℓ) (subsetPred : Pred A b) (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ ⊔ b) where
  field
    isSubGroup : IsSubGroup _≈_ subsetPred _∙_ ε _⁻¹
    isNormal : IsNormalInG isSubGroup U
  open IsSubGroup isSubGroup public

record NormalSubGroup c b ℓ : Set (suc (c ⊔ ℓ ⊔ b)) where
  infix  8 _⁻¹
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    IsInSubset : Pred Carrier b
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    ε       : Carrier
    _⁻¹     : Op₁ Carrier
    isNormalSubGroup : IsNormalSubGroup _≈_ IsInSubset _∙_ ε _⁻¹

  open IsNormalSubGroup isNormalSubGroup public

  subGroup : SubGroup c b ℓ 
  subGroup = record { isSubGroup  = isSubGroup }

  open SubGroup subGroup public using (semigroup; monoid; rawMonoid)

--Every subgroup of an abelian group is normal
everySubGroupOfAbelianIsNormal : {c b ℓ : Level} (g : AbelianGroup c ℓ) → let open AbelianGroup g in (SubsetPred : Pred Carrier b)
 → (subGroup : IsSubGroup _≈_ SubsetPred _∙_ ε _⁻¹) → IsNormalSubGroup _≈_ SubsetPred _∙_ ε _⁻¹
IsNormalSubGroup.isSubGroup (everySubGroupOfAbelianIsNormal g SubsetPred subGroup) = subGroup
IsNormalSubGroup.isNormal (everySubGroupOfAbelianIsNormal g@record { _≈_ = _≈_ ; _∙_ = _∙_ ; ε = ε ; _⁻¹ = _⁻¹ } SubsetPred isSubGroup) a x xInSubset =  let
  qq1 : (a ∙ x) ≈ (x ∙ a)
  qq1 = AbelianGroup.comm g a x
  qq2 : ((a ∙ x) ∙ (a ⁻¹)) ≈ ((x ∙ a) ∙ (a ⁻¹))
  qq2 = AbelianGroup.∙-cong g qq1  (AbelianGroup.refl g)
  qq3 : ((x ∙ a) ∙ (a ⁻¹)) ≈ (x ∙ (a ∙ (a ⁻¹)))
  qq3 = AbelianGroup.assoc g x a (a ⁻¹)
  qqw4 : (a ∙ (a ⁻¹)) ≈ ε
  qqw4 = proj₂ (g. AbelianGroup.inverse) a
  qqw5 : (x ∙ ε)  ≈ x
  qqw5 = proj₂ (AbelianGroup.identity g) x
  tr = AbelianGroup.trans g
  qqw6 : ( x ∙ (a ∙ (a ⁻¹)) ) ≈ (x ∙ ε)
  qqw6 = (AbelianGroup.∙-cong g) ((AbelianGroup.refl g) {x}) qqw4
  ee : ((a ∙ x) ∙ (a ⁻¹)) ≈ x
  ee =  tr qq2 (tr qq3 (tr qqw6 qqw5))
  in (IsSubGroup.≈_respect isSubGroup) (AbelianGroup.sym g ee) xInSubset
